Skip to content

Verify handwritten tycon constants against the Prelude (tconcheck); qualification-scoped tycon comparison#1046

Open
nanavati wants to merge 4 commits into
B-Lang-org:mainfrom
nanavati:tycon-drift-check
Open

Verify handwritten tycon constants against the Prelude (tconcheck); qualification-scoped tycon comparison#1046
nanavati wants to merge 4 commits into
B-Lang-org:mainfrom
nanavati:tycon-drift-check

Conversation

@nanavati

Copy link
Copy Markdown
Collaborator

Adds a build-time checker for an invariant the compiler already relies on, and aligns the tycon comparison instances with it.

The invariant

The front end enforces one type constructor per qualified name, so a qualified Id determines its (kind, sort) payload. This is already load-bearing in shipped comparison code: IType.cmpT compares ITCon by Id only (kind and sort ignored), and CType's Eq TyCon ignores the sort. But the compiler also carries handwritten copies of tycon payloads (Type.hs constants, ISyntaxUtil ITCon literals, StdPrel's seeded rows and tyConOf fields) with nothing keeping them in agreement with the Prelude — drift is silent precisely because the comparisons ignore the payload.

tconcheck

A new checker executable (built with the other utility exes) that obtains a Prelude symbol table through the production path — BinUtil.readImports on an in-memory probe package, replaceImportedSignatures for full-defs signatures (needed: Pred__/SchedPragma are declared but not exported), MakeSymTab.mkSymTab — and verifies 94 entries across three registries: Type.handwrittenTCons (40), ISyntaxUtil.handwrittenITCons (32), and StdPrel's preTypes rows and preClasses' tyConOf twins (22). Registries are co-located beneath the constants they cover.

It is wired as a build step: make install-src runs it right after the libraries build and fails on any unwaived drift (drift produces a compiler whose type comparisons are silently wrong — the artifact should not be produced). A thin testsuite wrapper (bsc.misc/tcon_drift) additionally checks installed artifacts for self-coherence.

What it found on its first run

Nine real drifts, all masked today by the payload-ignoring comparisons: six stale sorts in Type.hs (Int/UInt claim TIabstract vs Prelude's TIdata; PrimPair claims SStruct vs SInterface; ActionValue claims a struct sort vs TIdata; ActionValue_ has stale field names; File claims TIabstract), and three on the ISyntax side including two kind bugs: itInout has kind # -> * (the real Inout is * -> *), and itPrimPair's kind is left-nested because IKFun has no fixity declaration (Haskell defaults to infixl 9, so backticked kind chains parse backwards). A follow-up commit on this branch fixes all nine and declares the fixity, shrinking the waiver list to empty.

Comparison alignment

Eq/Ord TyCon become qualification-scoped: when both Ids are qualified (the invariant's domain), comparison is by Id; when either is unqualified — where an Id is a scope query, not a name, and the invariant is undefined — the existing kind hedge is kept. The instances now document the semantics that were previously implicit: Eq TyCon is deliberately non-transitive via qualEq (scope-resolution fuzz), Eq and Ord disagree (containers key on the lawful Ord), and cmpT's by-Id ITCon comparison is justified by the invariant (all ITCon Ids are qualified — IType is born post-resolution at IConv) rather than by an unstated assumption. An audit found no comparison site that mixes kind-resolved and unresolved tycons of the same qualified name (qualification and kind-filling happen together in MakeSymTab.convCQType; boundary code uses kind-agnostic helpers).

Validation

Full testsuite: 19046 PASS / 0 FAIL / 129 XFAIL / 0 XPASS. The build gate demonstrably works (it failed the build on the nine drifts before they were waived/fixed). The checker result is identical against pre-change and post-change compilers and freshly rebuilt libraries.

This also prepares the ground for hash-consing IType (planned follow-up): interning wants Id-determines-payload to be a checked invariant rather than folklore.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK

nanavati and others added 4 commits July 14, 2026 09:41
Generic.everywhere rebuilds every node of the IModule whether
changed or not; the transformation only rewrites ICon identifiers.
An explicit traversal covers the same reachable ICon sites (heap
references are leaves either way, since the cells sit behind
IORefs), preserves untouched subtrees instead of reallocating
them, and answers the old XXX about IAps recursion explicitly.

bluetcl's find_vmodinfo becomes a direct query (ICVerilog is the
only VModInfo carrier reachable in an IPackage), and with the last
generic traversals gone, the Data/Typeable derivings on ISyntax
and HeapData are removed.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012KHVhEzJpur1ZRjNjpzBVj
BSC's front end enforces one type constructor per qualified name, so a
qualified Id determines its (kind, sort) payload.  Shipped comparison
code already relies on this invariant (TyCon Eq ignores the sort; ITCon
comparison is by Id alone), but nothing checked the compiler's
handwritten copies of Prelude tycon payloads against the Prelude truth.

Add a tconcheck utility that obtains a Prelude symbol table the
production way (BinUtil.readImports on an in-memory probe package, the
full all-defs signatures via BinUtil.replaceImportedSignatures exactly
as bsc's module-generation symtab does, then MakeSymTab.mkSymTab) and
verifies, entry by entry:

  * every registered Type.hs TCon constant (new registry
    Type.handwrittenTCons, 40 entries): Maybe Kind and TISort
  * every registered ISyntaxUtil/IType ITCon constant (new registry
    ISyntaxUtil.handwrittenITCons, 32 entries): IKind via IConv.iConvK
    (newly exported) and TISort
  * every StdPrel.preTypes row against the symbol table
  * every StdPrel.preClasses tyConOf payload, both against the symbol
    table and against its preTypes twin row (these are seeded through
    independent paths in MakeSymTab with nothing else enforcing
    agreement)

The check runs as part of the build (src/Libraries/Makefile), pointed
at the just-built libraries, so a Prelude edit that changes a payload
fails the build instead of silently drifting; tconcheck is built and
installed with the standard comp install for that purpose.  A thin
testsuite wrapper (testsuite/bsc.misc/tcon_drift) re-checks the
installed tools.

The checker found nine pre-existing drifts, masked until now by the
payload-ignoring comparisons; they are documented and waived (loudly)
in tconcheck.knownDrift pending direction, e.g. Type.hs still calls
Int/UInt/File abstract although the Prelude declares them as data
types, ISyntaxUtil.itInout has kind # -> * although Inout is * -> *,
and itPrimPair's kind is left-nested because IKFun has no fixity
declaration.

In lifting the inline ITCon literals out of itPair/itList/itMaybe so
they could be registered (itPrimPair, itListCon, itMaybeCon), the
expressions are kept verbatim; no behavior change.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
BSC's front end enforces one type constructor per qualified name, so a
qualified Id determines its (kind, sort) payload.  This invariant was
already load-bearing in comparison code -- TyCon Eq ignored the sort,
and ITCon comparison in IType.cmpT is by Id alone -- but unstated, and
the TyCon instances mixed regimes: Eq compared kinds even for pairs
where the invariant makes that a dead tail, while remaining
kind-sensitive for the unqualified names where the invariant is
undefined.

Scope the TyCon comparisons by qualification:

  * Eq: both-qualified pairs compare by Id (qualEq); the kind hedge is
    kept only when either side is unqualified (resolution-era fuzz).
  * Ord: lexicographic on (base, qual); within a (base, qual) bucket,
    both-qualified ties are EQ without consulting the kinds, and the
    unqualified bucket keeps the kind comparison.  This remains a
    lawful total order.

Document at the instances: the invariant and its qualified-only domain,
the deliberate non-transitivity of Eq via qualEq (pre-existing), the
Eq/Ord disagreement (pre-existing; containers key on Ord), and the
pointer to the tconcheck build step that verifies the handwritten
payload copies the by-Id comparisons rely on.  Also upgrade the cmpT
comment in IType.hs: ITCon by-Id comparison is justified by the same
invariant (all ITCon Ids are qualified, since IType is born
post-resolution at IConv); the ITForAll binder-kind skip is a separate,
alpha-structural assumption, unchanged.

The only behavior delta is a both-qualified pair with the same name and
differing Maybe Kind fields.  An audit of the pipeline found no
comparison site where a qualified Nothing-kinded TyCon (parse-era
trees, cTCon-built compiler-generated code) can meet its Just-kinded
twin (symtab/convCQType-era types): type-level Eq/Ord is only exercised
within a single kind regime, cross-regime checks use kind-agnostic
helpers (leftCon, mkInstId, Id comparisons), and no container is keyed
on Type/CType where mixed twins could coexist.  The full testsuite and
a rebuild of all libraries with the changed compiler back this
empirically.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Bring all nine drifted constants in line with the Prelude-derived truth
(the checker's DRIFT output was used as the spec), and empty the
tconcheck knownDrift waiver list; the waiver mechanism remains for
future incidents but ships empty.

  * Type.hs tInt/tUInt: TIabstract -> TIdata (Prelude declares
    'data Int n = Int (Bit n)' and likewise UInt)
  * Type.hs tPrimPair (and StdPrel tiPair, used by itPrimPair):
    SStruct -> SInterface [] (PrimPair is declared as an interface)
  * Type.hs tActionValue: old struct sort -> TIdata [ActionValue]
    ('data ActionValue a = ActionValue ...')
  * Type.hs tActionValue_: field names __value/__action ->
    avValue_/avAction_ (new PreIds position variants added)
  * Type.hs tFile: TIabstract -> TIdata [InvalidFile, MCD, FD]
    (new PreStrings/PreIds constructor ids added)
  * ISyntaxUtil itInout: kind # -> * (apparently copied from itInout_)
    corrected to * -> *
  * ISyntaxUtil itPrimPair: kind was left-nested, (* -> *) -> *,
    because IKFun had no fixity declaration and defaulted to infixl 9;
    IType.hs now declares infixr 8 `IKFun` (matching Kind's right-nested
    Kfun and IConv.iConvK).  Census of every backticked IKFun chain in
    the tree: itPrimPair was the only unparenthesized multi-arrow chain;
    all others are single-arrow or already explicitly parenthesized, so
    the fixity change reparses nothing else.
  * StdPrel tiBufferMode (used by itBufferMode): tiEnum -> tiData
    (BlockBuffering carries a Maybe Integer argument, so BufferMode is
    not an enum)

The corresponding position-parameterized variants (tIntAt,
tActionValueAt, tActionValue_At) are fixed to the same payloads.

A consumer audit found no reader of these payloads out of the constants
themselves: comparison sites use Eq/Ord (which compare by qualified Id)
or wildcard the payload fields in patterns; the payloads only travel
into generated ISyntax via iConvT, where they now agree with what
symtab-derived types already carried.

tconcheck now reports all 94 entries OK with zero waived.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant